es:ES, ds:x:Id fp Type, T:Type, i:Id, f:(State(ds)T).
(x, y:T. Dec(x = y))
 (x:Id. vartype(i;x) r ds(x)?Top)
 e'@i.
 (e<e'. f((state when e)) = f((state when e')))
  (e:E
  (((e <loc e')
  (c (((f((state when e)) = f((state when e'))))
  (c & (e'':E.
  (c & ((e <loc e'')
  (c & ( e'' loc e' 
  (c & ( (f((state when e'')) = f((state when e'))  T))))) 

latex

Definitions

x:A. B(x), State(ds), P  Q, e@i. P(e), P  Q, x:A. B(x), A c B, (e <loc e'), P & Q, e loc e' , , t  T, x. t(x), state@i, e<e'. P(e), T, True, A, {T}, P  Q, x(s), P  Q, False, Dec(P)

Lemmas

alle-at-iff, alle-lt wf, es-loc wf, es-state-when wf, subtype rel dep function, es-vartype wf, fpf-cap wf, id-deq wf, top wf, subtype rel self, es-causl wf, not wf, es-loc-pred, es-locl-iff, es-locl wf, es-le-loc, assert wf, es-first wf, Id wf, decidable wf, decl-state wf, fpf wf, event system wf, es-le wf, squash wf, true wf, es-E wf, es-pred-locl, es-locl transitivity2, es-le weakening, es-le-iff, es-axioms